$M$.rframe($k$ reads $x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$L$ != ($M$.2.2.2.2.2.2.2.2.2.2).1($x$) $\Rightarrow$ $\uparrow$deq{-}member(KindDeq;$k$;$L$)